| Definitions | False, P   Q,  A, t  T,  x:A. B(x),  b,  b,  , s = t, Prop, IdDeq, Id, Type,  x.A(x), x. t(x), f(x), A B,  , {x:A| B(x) },  , a:A fp B(a), Top, x:A B(x), x dom(f), x:A B(x), P & Q, P  Q, Unit, left+right, f(x)?z, kind(e), Valtype(da;k), valtype(e), isrcv(e), P  Q, 1of(t), E, if b t else f fi, KindDeq, Knd, Case b of inl(x) s(x) ; inr(y) t(y), Atom$n, rec(x.A(x)), ecl(ds;da), ES, es-decls(es;i;ds;da), val(e), Void, {T}, SQType(T), s ~ t, State(ds), #$n, True,  T, 2of(t), <a,b>, vartype(i;x), state@i, (state when e), f(a), loc(e), A/x,y. B(x;y), es-init(es;e), action[[a n]][e1;e2], x when e, nil, product-deq(A;B;a;b), type List, x,y. t(x;y), list_accum(x,a.f(x;a);y;l), (x after e), EqDecider(T), e@i. P(e), @i[[x;upd]], update-spec(ds;da) |